<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<HTML>
<HEAD>
<TITLE>The CompCert verified compiler</TITLE>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">

<style type="text/css">
body {
  color: black; background: white;
  margin-left: 5%; margin-right: 5%;
  max-width:750px;
}
h2 { margin-left: -5%;}
h3 { margin-left: -3%; }
h1,h2,h3 { font-family: sans-serif; }
hr { margin-left: -5%; margin-right:-5%; }
a:visited {color : #416DFF; text-decoration : none; font-weight : bold}
a:link {color : #416DFF; text-decoration : none; font-weight : bold}
a:hover {color : Red; text-decoration : underline; }
a:active {color : Red; text-decoration : underline; }
</style>

</HEAD>
<BODY>

<H1 align="center">The CompCert verified compiler</H1>
<H2 align="center">Commented Coq development</H2>
<H3 align="center">Version 3.16, 2025-09-01</H3>

<H2>Introduction</H2>

<P>CompCert is a compiler that generates ARM, PowerPC, RISC-V and x86 assembly
code from CompCert C, a large subset of the C programming language.
The particularity of this compiler is that it is written mostly within
the specification language of the Coq proof assistant, and its
correctness --- the fact that the generated assembly code is
semantically equivalent to its source program --- was entirely proved
within the Coq proof assistant.</P>

<P>High-level descriptions of the CompCert compiler and its proof of 
correctness can be found in the following papers (in increasing order of technical details):</P>
<UL>
<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. 
Journal of Automated Reasoning 43(4):363-446, 2009.
</UL>

<P>This Web site gives a commented listing of the underlying Coq
specifications and proofs.  Proof scripts are folded by default, but
can be viewed by clicking on "Proof".  Some modules (written in <I>italics</I> below) differ between the five target architectures.  The
PowerPC versions of these modules are shown below; the AArch64, ARM,
x86 and RISC-V versions can be found in the source distribution.
</P>

<P> This development is a work in progress; some parts have
substantially changed since the overview papers above were
written.</P>

<P>The complete sources for CompCert can be downloaded from
<A HREF="https://github.com/AbsInt/CompCert/">the Git repository</A>
or <A HREF="https://compcert.org/">the CompCert Web site</A>.
</P>

<P>This document and the CompCert sources are copyright Institut
National de Recherche en Informatique et en Automatique (INRIA) and
AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the
following <A HREF="LICENSE.txt">license</A>.
</P>

<H2>Table of contents</H2>

<H3>General-purpose libraries, data structures and algorithms</H3>

<UL>
<LI> <A HREF="html/compcert.lib.Coqlib.html">Coqlib</A>: addendum to the Coq standard library.
<LI> <A HREF="html/compcert.lib.Maps.html">Maps</A>: finite maps.
<LI> <A HREF="html/compcert.lib.Integers.html">Integers</A>: machine integers.
<LI> <A HREF="html/compcert.lib.Floats.html">Floats</A>: machine floating-point numbers.
<LI> <A HREF="html/compcert.lib.Iteration.html">Iteration</A>: various forms of "while" loops.
<LI> <A HREF="html/compcert.lib.Ordered.html">Ordered</A>: construction of
ordered types.
<LI> <A HREF="html/compcert.lib.Lattice.html">Lattice</A>: construction of
semi-lattices.
<LI> <A HREF="html/compcert.backend.Kildall.html">Kildall</A>: resolution of dataflow
inequations by fixpoint iteration.
<LI> <A HREF="html/compcert.lib.UnionFind.html">UnionFind</A>: a persistent union-find data structure.
<LI> <A HREF="html/compcert.lib.Postorder.html">Postorder</A>: postorder numbering of a directed graph.
</UL>

<H3>Definitions and theorems used in many parts of the development</H3>

<UL>
<LI> <A HREF="html/compcert.common.Errors.html">Errors</A>: the Error monad.
<LI> <A HREF="html/compcert.common.AST.html">AST</A>: identifiers, whole programs and other
common elements of abstract syntaxes.
<LI> <A HREF="html/compcert.common.Linking.html">Linking</A>: generic framework to define syntactic linking over the CompCert languages.
<LI> <A HREF="html/compcert.common.Values.html">Values</A>: run-time values.
<LI> <A HREF="html/compcert.common.Events.html">Events</A>: observable events and traces.
<LI> <A HREF="html/compcert.common.Memory.html">Memory</A>: memory model. <BR>
See also: <A HREF="html/compcert.common.Memdata.html">Memdata</A> (in-memory representation of data).
<LI> <A HREF="html/compcert.common.Globalenvs.html">Globalenvs</A>: global execution environments.
<LI> <A HREF="html/compcert.common.Smallstep.html">Smallstep</A>: tools for small-step semantics.
<LI> <A HREF="html/compcert.common.Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs.
<LI> <A HREF="html/compcert.common.Determinism.html">Determinism</A>: determinism properties of small-step semantics.
<LI> <A HREF="html/compcert.powerpc.Op.html"><I>Op</I></A>: operators, addressing modes and their
semantics.
<LI> <A HREF="html/compcert.common.Builtins.html">Builtins</A>: semantics of built-in functions. <BR>
See also: <A HREF="html/compcert.common.Builtins0.html">Builtins0</A> (target-independent part), <A HREF="html/compcert.powerpc.Builtins1.html"><I>Builtins1</I></A> (target-dependent part).
<LI> <A HREF="html/compcert.common.Unityping.html">Unityping</A>: a solver for atomic unification constraints.
</UL>

<H3>Source, intermediate and target languages: syntax and semantics</H3>

<UL>
<LI> The CompCert C source language:
<A HREF="html/compcert.cfrontend.Csyntax.html">syntax</A> and
<A HREF="html/compcert.cfrontend.Csem.html">semantics</A> and
<A HREF="html/compcert.cfrontend.Cstrategy.html">determinized semantics</A> and
<A HREF="html/compcert.cfrontend.Ctyping.html">type system</A>.<BR>
See also: <A HREF="html/compcert.cfrontend.Ctypes.html">type expressions</A> and
<A HREF="html/compcert.cfrontend.Cop.html">operators (syntax and semantics)</A>.<BR>
See also: <A HREF="html/compcert.cfrontend.Cexec.html">reference interpreter</A>.
<LI> <A HREF="html/compcert.cfrontend.Clight.html">Clight</A>: a simpler version of CompCert C where expressions contain no side-effects.
<LI> <A HREF="html/compcert.cfrontend.Csharpminor.html">Csharpminor</A>: low-level
 structured language.
<LI> <A HREF="html/compcert.backend.Cminor.html">Cminor</A>: low-level structured
language, with explicit stack allocation of certain local variables.
<LI> <A HREF="html/compcert.backend.CminorSel.html">CminorSel</A>: like Cminor,
with machine-specific operators and addressing modes.
<LI> <A HREF="html/compcert.backend.RTL.html">RTL</A>: register transfer language (3-address
code, control-flow graph, infinitely many pseudo-registers). <BR>
See also: <A HREF="html/compcert.backend.Registers.html">Registers</A> (representation of
pseudo-registers).
<LI> <A HREF="html/compcert.backend.LTL.html">LTL</A>: location transfer language (3-address
code, control-flow graph of basic blocks, finitely many physical registers, infinitely
many stack slots). <BR>
See also: <A HREF="html/compcert.backend.Locations.html">Locations</A> (representation of
locations) and <A HREF="html/compcert.powerpc.Machregs.html"><I>Machregs</I></A> (description of processor registers).
<LI> <A HREF="html/compcert.backend.Linear.html">Linear</A>: like LTL, but the CFG is
replaced by a linear list of instructions with explicit branches and labels.
<LI> <A HREF="html/compcert.backend.Mach.html">Mach</A>: like Linear, with a more concrete
view of the activation record.  
<LI> <A HREF="html/compcert.powerpc.Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly
code.
</UL>

<H3>Compiler passes</H3>

<TABLE cellpadding="5%">
<TR valign="top">
  <TH>Pass</TH>
  <TH>Source &amp; target</TH>
  <TH>Compiler&nbsp;code</TH>
  <TH>Correctness&nbsp;proof</TH>
</TR>

<TR valign="top">
  <TD>Pulling side-effects out of expressions;<br>
      fixing an evaluation order</TD>
  <TD>CompCert C to Clight</TD>
  <TD><A HREF="html/compcert.cfrontend.SimplExpr.html">SimplExpr</A></TD>
  <TD><A HREF="html/compcert.cfrontend.SimplExprspec.html">SimplExprspec</A><br>
      <A HREF="html/compcert.cfrontend.SimplExprproof.html">SimplExprproof</A></TD>
</TR>
<TR valign="top">
  <TD>Pulling non-adressable scalar local variables out of memory</TD>
  <TD>Clight to Clight</TD>
  <TD><A HREF="html/compcert.cfrontend.SimplLocals.html">SimplLocals</A></TD>
  <TD><A HREF="html/compcert.cfrontend.SimplLocalsproof.html">SimplLocalsproof</A></TD>
</TR>
<TR valign="top">
  <TD>Simplification of control structures; <br>
      explication of type-dependent computations</TD>
  <TD>Clight to Csharpminor</TD>
  <TD><A HREF="html/compcert.cfrontend.Cshmgen.html">Cshmgen</A></TD>
  <TD><A HREF="html/compcert.cfrontend.Cshmgenproof.html">Cshmgenproof</A></TD>
</TR>
<TR valign="top">
  <TD>Stack allocation of local variables<br>
      whose address is taken;<br>
      simplification of switch statements</TD>
  <TD>Csharpminor to Cminor</TD>
  <TD><A HREF="html/compcert.cfrontend.Cminorgen.html">Cminorgen</A></TD>
  <TD><A HREF="html/compcert.cfrontend.Cminorgenproof.html">Cminorgenproof</A></TD>
</TR>

<TR valign="top">
  <TD>Recognition of operators<br>and addressing modes;<br>
      if-conversion</TD>
  <TD>Cminor to CminorSel</TD>
  <TD><A HREF="html/compcert.backend.Selection.html">Selection</A><br>
      <A HREF="html/compcert.powerpc.SelectOp.html"><I>SelectOp</I></A><br>
      <A HREF="html/compcert.powerpc.SelectLong.html"><I>SelectLong</I></A><br>
      <A HREF="html/compcert.backend.SelectDiv.html">SelectDiv</A><br>
      <A HREF="html/compcert.backend.SplitLong.html">SplitLong</A></TD>
  <TD><A HREF="html/compcert.backend.Selectionproof.html">Selectionproof</A><br>
      <A HREF="html/compcert.powerpc.SelectOpproof.html"><I>SelectOpproof</I></A><br>
      <A HREF="html/compcert.powerpc.SelectLongproof.html"><I>SelectLongproof</I></A><br>
      <A HREF="html/compcert.backend.SelectDivproof.html">SelectDivproof</A><br>
      <A HREF="html/compcert.backend.SplitLongproof.html">SplitLongproof</A></TD>
</TR>

<TR valign="top">
  <TD>Construction of the CFG; 3-address code generation</TD>
  <TD>CminorSel to RTL</TD>
  <TD><A HREF="html/compcert.backend.RTLgen.html">RTLgen</A></TD>
  <TD><A HREF="html/compcert.backend.RTLgenspec.html">RTLgenspec</A><BR>
      <A HREF="html/compcert.backend.RTLgenproof.html">RTLgenproof</A></TD>
</TR>

<TR valign="top">
  <TD>Recognition of tail calls</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/compcert.backend.Tailcall.html">Tailcall</A></TD>
  <TD><A HREF="html/compcert.backend.Tailcallproof.html">Tailcallproof</A></TD>
</TR>

<TR valign="top">
  <TD>Function inlining</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/compcert.backend.Inlining.html">Inlining</A></TD>
  <TD><A HREF="html/compcert.backend.Inliningspec.html">Inliningspec</A><BR>
      <A HREF="html/compcert.backend.Inliningproof.html">Inliningproof</A></TD>
</TR>

<TR valign="top">
  <TD>Postorder renumbering of the CFG</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
</TR>

<TR valign="top">
  <TD>Constant propagation</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/compcert.backend.Constprop.html">Constprop</A><br>
      <A HREF="html/compcert.powerpc.ConstpropOp.html"><I>ConstpropOp</I></A></TD>
  <TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br>
      <A HREF="html/compcert.powerpc.ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
</TR>

<TR valign="top">
  <TD>Common subexpression elimination</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR>
      <A HREF="html/compcert.powerpc.CombineOp.html"><I>CombineOp</I></A></TD>
  <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR>
      <A HREF="html/compcert.powerpc.CombineOpproof.html"><I>CombineOpproof</I></A></TD>
</TR>

<TR valign="top">
  <TD>Redundancy elimination</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/compcert.backend.Deadcode.html">Deadcode</A></TD>
  <TD><A HREF="html/compcert.backend.Deadcodeproof.html">Deadcodeproof</A></TD>
</TR>

<TR valign="top">
  <TD>Removal of unused static globals</TD>
  <TD>RTL to RTL</TD>
  <TD><A HREF="html/compcert.backend.Unusedglob.html">Unusedglob</A></TD>
  <TD><A HREF="html/compcert.backend.Unusedglobproof.html">Unusedglobproof</A></TD>
</TR>

<TR valign="top">
  <TD>Register allocation (validation a posteriori)</TD>
  <TD>RTL to LTL</TD>
  <TD><A HREF="html/compcert.backend.Allocation.html">Allocation</A></TD>
  <TD><A HREF="html/compcert.backend.Allocproof.html">Allocproof</A></TD>
</TR>

<TR valign="top">
  <TD>Branch tunneling</TD>
  <TD>LTL to LTL</TD>
  <TD><A HREF="html/compcert.backend.Tunneling.html">Tunneling</A></TD>
  <TD><A HREF="html/compcert.backend.Tunnelingproof.html">Tunnelingproof</A></TD>
</TR>

<TR valign="top">
  <TD>Linearization of the CFG</TD>
  <TD>LTL to Linear</TD>
  <TD><A HREF="html/compcert.backend.Linearize.html">Linearize</A></TD>
  <TD><A HREF="html/compcert.backend.Linearizeproof.html">Linearizeproof</A></TD>
</TR>

<TR valign="top">
  <TD>Removal of unreferenced labels</TD>
  <TD>Linear to Linear</TD>
  <TD><A HREF="html/compcert.backend.CleanupLabels.html">CleanupLabels</A></TD>
  <TD><A HREF="html/compcert.backend.CleanupLabelsproof.html">CleanupLabelsproof</A></TD>
</TR>

<TR valign="top">
  <TD>Synthesis of debugging information</TD>
  <TD>Linear to Linear</TD>
  <TD><A HREF="html/compcert.backend.Debugvar.html">Debugvar</A></TD>
  <TD><A HREF="html/compcert.backend.Debugvarproof.html">Debugvarproof</A></TD>
</TR>

<TR valign="top">
  <TD>Laying out the activation records</TD>
  <TD>Linear to Mach</TD>
  <TD><A HREF="html/compcert.backend.Stacking.html">Stacking</A><BR>
      <A HREF="html/compcert.backend.Bounds.html">Bounds</A><BR>
      <A HREF="html/compcert.powerpc.Stacklayout.html"><I>Stacklayout</I></A></TD>
  <TD><A HREF="html/compcert.backend.Stackingproof.html">Stackingproof</A><br>
      <A HREF="html/compcert.common.Separation.html">Separation</A></TD>
</TR>

<TR valign="top">
  <TD>Emission of assembly code</TD>
  <TD>Mach to Asm</TD>
  <TD><A HREF="html/compcert.powerpc.Asmgen.html"><I>Asmgen</I></A></TD>
  <TD><A HREF="html/compcert.backend.Asmgenproof0.html"><I>Asmgenproof0</I></A><BR>
      <A HREF="html/compcert.powerpc.Asmgenproof1.html"><I>Asmgenproof1</I></A><BR>
      <A HREF="html/compcert.powerpc.Asmgenproof.html"><I>Asmgenproof</I></A></TD>
</TR>
</TABLE>

<H3>All together</H3>

<UL>
<LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together;
whole-compiler semantic preservation theorems.
<LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
</UL>

<H3>Static analyses</H3>

The following static analyses are performed over the RTL intermediate
representation to support optimizations such as constant propagation,
CSE, and dead code elimination.
<UL>
<LI> <A HREF="html/compcert.backend.Liveness.html">Liveness</A>: liveness analysis</A>.
<LI> <A HREF="html/compcert.backend.ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR>
See also: <A HREF="html/compcert.backend.ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR>
See also: <A HREF="html/compcert.powerpc.ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis.
<LI> <A HREF="html/compcert.backend.Deadcode.html">Deadcode</A>: neededness analysis</A> <BR>
See also: <A HREF="html/compcert.backend.NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR>
See also: <A HREF="html/compcert.powerpc.NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis.
</UL>

<H3>Type systems</H3>

The <A HREF="html/compcert.cfrontend.Ctyping.html">type system of CompCert C</A> is fully formalized.  For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
<UL>
<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">Ctyping</A>: typing for CompCert C + type-checking functions.
<LI> <A HREF="html/compcert.backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type
reconstruction.
<LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear.
</UL>

<HR>
<ADDRESS>xavier.leroy@college-de-france.fr</ADDRESS>
<HR>

</BODY>
</HTML>
